Nuprl Definition : R-Feasible 11,40

R-Feasible{i:l}
R-Feasible(R)
== es_realizer_ind(R;
== es_realizer_ind(True;
== es_realizer_ind(left,right,rec1,rec2.(rec1  rec2  R-compat{i:l}(leftright));
== es_realizer_ind(loc,T,x,v.True;
== es_realizer_ind(loc,T,x,L.normal-type{i:l}
== es_realizer_ind(loc,T,x,L.normal-type(T);
== es_realizer_ind(lnk,tag,L.True;
== es_realizer_ind(loc,ds,knd,T,x,f.((normal-ds{i:l}(ds normal-type{i:l}(T))
== es_realizer_ind( ((isrcv(knd))  (loc = destination(lnk(knd)))));
== es_realizer_ind(ds,knd,T,l,dt,g.(((isrcv(knd))
== es_realizer_ind(ds,knd,T,l,dt,g.( (((eq_lnk(lnk(knd); l))
== es_realizer_ind(ds,knd,T,l,dt,g.(  (T = fpf-cap(dt; id-deq; tag(knd); void)))
== es_realizer_ind(ds,knd,T,l,dt,g.(  (destination(lnk(knd)) = source(l))))
== es_realizer_ind( (normal-type{i:l}(T normal-ds{i:l}(ds))
== es_realizer_ind( normal-ds{i:l}
== es_realizer_ind( normal-ds(dt));
== es_realizer_ind(loc,ds,a,T,P.normal-ds{i:l}
== es_realizer_ind(loc,ds,a,T,P.normal-ds(ds);
== es_realizer_ind(loc,k,L.True;
== es_realizer_ind(loc,k,L.True;
== es_realizer_ind(loc,x,L.True) 
latex



clarification:

R-Feasible{i:l}
R-Feasible(R)
== es_realizer_ind(R;
== es_realizer_ind(True;
== es_realizer_ind(left,right,rec1,rec2.(rec1  rec2  R-compat{i:l}(leftright));
== es_realizer_ind(loc,T,x,v.True;
== es_realizer_ind(loc,T,x,L.normal-type{i:l}
== es_realizer_ind(loc,T,x,L.normal-type(T);
== es_realizer_ind(lnk,tag,L.True;
== es_realizer_ind(loc,ds,knd,T,x,f.((normal-ds{i:l}(ds normal-type{i:l}(T))
== es_realizer_ind( ((isrcv(knd))  (loc = destination(lnk(knd))  Id)));
== es_realizer_ind(ds,knd,T,l,dt,g.(((isrcv(knd))
== es_realizer_ind(ds,knd,T,l,dt,g.( (((eq_lnk(lnk(knd); l))
== es_realizer_ind(ds,knd,T,l,dt,g.(  (T = fpf-cap(dt; id-deq; tag(knd); void)  Type{i}))
== es_realizer_ind(ds,knd,T,l,dt,g.(  (destination(lnk(knd)) = source(l Id)))
== es_realizer_ind( (normal-type{i:l}(T normal-ds{i:l}(ds))
== es_realizer_ind( normal-ds{i:l}
== es_realizer_ind( normal-ds(dt));
== es_realizer_ind(loc,ds,a,T,P.normal-ds{i:l}
== es_realizer_ind(loc,ds,a,T,P.normal-ds(ds);
== es_realizer_ind(loc,k,L.True;
== es_realizer_ind(loc,k,L.True;
== es_realizer_ind(loc,x,L.True) 
latex


Definitionses realizer ind, R-compat{i:l}(AB), isrcv(k), P  Q, b, eq_lnk(ab), Type, fpf-cap(feqxz), id-deq, tag(k), void, s = t, Id, destination(l), lnk(k), source(l), P  Q, normal-type{i:l}(T), normal-ds{i:l}(ds), True
FDL editor aliasesR-Feasible

origin